\begin{tabbing}
d{-}chooser($D$;${\it dec}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$j$:Id, $b$:Id, $s$:d{-}m($D$; $j$).state.\+
\\[0ex](\=isl(${\it dec}$($j$,$b$,$s$))\+
\\[0ex]$\Leftrightarrow$
\\[0ex]$b$ in dom(d{-}m($D$; $j$).pre) \& ($\exists$$v$:d{-}m($D$; $j$).da(locl($b$)). d{-}m($D$; $j$).pre($b$,$s$,$v$)))
\-\\[0ex]\& (isl(${\it dec}$($j$,$b$,$s$)) $\Rightarrow$ $b$ in dom(d{-}m($D$; $j$).pre) \& d{-}m($D$; $j$).pre($b$,$s$,outl(${\it dec}$($j$,$b$,$s$))))
\-
\end{tabbing}